# Copyright 1999-2004 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $

EAPI="2"
inherit eutils

DESCRIPTION="Why - a multi-language multi-prover verification tool"
HOMEPAGE="http://why.lri.fr/index.en.html"
SRC_URI="http://why.lri.fr/download/${P}.tar.gz"

LICENSE="LGPL"
SLOT="0"
KEYWORDS="x86 sparc"

IUSE="coq cvc3 frama-c gappa pvs simplify"
DEPEND="
    >=dev-lang/ocaml-3.07
    >=dev-ml/lablgtk-2.6.0
    dev-ml/ocamlgraph
    coq? ( >=sci-mathematics/coq-7.0 )
    pvs? ( sci-mathematics/pvs )
    gappa? ( sci-mathematics/gappa )
    cvc3? ( sci-libs/cvc3 )
    frama-c? ( =sci-mathematics/frama-c-20100401 )
    simplify? ( sci-mathematics/simplify )
  "
RDEPEND="${DEPEND}"

src_unpack() {
	unpack ${A}
	cd "${S}"
	epatch "${FILESDIR}/${P}-ocamlgraph-pvs.patch"
}

src_compile() {
	econf || die

	myconf="PVSLIB=/opt/pvs/lib"
	make ${myconf} || die
}

src_install() {
	local FRAMAC_LIBDIR=${D}usr/lib/frama-c
	local FRAMAC_PLUGINDIR=${FRAMAC_LIBDIR}/plugins
	local FRAMAC_SHAREDIR=${D}usr/share/frama-c
	local myconf="COQLIB=${D}usr/lib/coq \
		PVSLIB=${D}opt/pvs/lib \
		DESTDIR=${D} \
		FRAMAC_PLUGINDIR=${FRAMAC_PLUGINDIR}
		FRAMAC_SHARE=${FRAMAC_SHAREDIR}
		FRAMAC_LIBDIR=${FRAMAC_LIBDIR}"
	if use frama-c || -f /usr/bin/frama-c; then
		mkdir -p ${FRAMAC_PLUGINDIR}
		mkdir -p ${FRAMAC_SHAREDIR}
		cp -r /usr/share/frama-c/* ${FRAMAC_SHAREDIR}/
		sed -i 's/>> $(FRAMAC_SHARE)\/known_plugins.ac/""/g' ${FRAMAC_SHAREDIR}/known_plugins.ac
	fi
	make $myconf install || die
	if use frama-c || -f /usr/bin/frama-c; then
		rm -rf ${FRAMAC_SHAREDIR}
	fi
}

pkg_postinst() {
	if use frama-c || -f /usr/bin/frama-c; then
		ewarn "Please run the following command after Why is installed:"
		ewarn ""
		ewarn "  echo ENABLE_JESSIE=yes >> /usr/share/frama-c/known_plugins.ac"
	fi
}
